CBMC: Improve proof stability #611

mkannwischer · 2025-11-05T02:53:03Z

This hoists @rod-chapman's work to fix and stabilize CBMC proofs in #558.
The changes are independent of the changes in #558, so we should review and merge them separately.

Resolves CBMC proof performance regression #547

mldsa/src/polyvec.c

mkannwischer · 2025-11-05T03:09:08Z

Proof runtime in CI improves significantly:

ML-DSA-44: 9m -> 6m
ML-DSA-65: 8m -> 7m
ML-DSA-87: 11m -> 9m

More importantly: It makes proofs in #558 feasible.

github-actions

Mac Mini (M1, 2020) benchmarks (opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`46329` cycles	`46218` cycles	`1.00`
`ML-DSA-44 sign`	`132740` cycles	`132732` cycles	`1.00`
`ML-DSA-44 verify`	`47859` cycles	`47856` cycles	`1.00`
`ML-DSA-65 keypair`	`81166` cycles	`81143` cycles	`1.00`
`ML-DSA-65 sign`	`219425` cycles	`219230` cycles	`1.00`
`ML-DSA-65 verify`	`80176` cycles	`80142` cycles	`1.00`
`ML-DSA-87 keypair`	`132372` cycles	`132363` cycles	`1.00`
`ML-DSA-87 sign`	`281076` cycles	`280899` cycles	`1.00`
`ML-DSA-87 verify`	`130457` cycles	`130331` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Mac Mini (M1, 2020) benchmarks (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`115037` cycles	`115058` cycles	`1.00`
`ML-DSA-44 sign`	`430858` cycles	`431610` cycles	`1.00`
`ML-DSA-44 verify`	`122162` cycles	`122198` cycles	`1.00`
`ML-DSA-65 keypair`	`197056` cycles	`197086` cycles	`1.00`
`ML-DSA-65 sign`	`701050` cycles	`701047` cycles	`1.00`
`ML-DSA-65 verify`	`197826` cycles	`197718` cycles	`1.00`
`ML-DSA-87 keypair`	`325230` cycles	`325233` cycles	`1.00`
`ML-DSA-87 sign`	`884603` cycles	`884671` cycles	`1.00`
`ML-DSA-87 verify`	`328995` cycles	`328825` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`34883` cycles	`34777` cycles	`1.00`
`ML-DSA-44 sign`	`120165` cycles	`120073` cycles	`1.00`
`ML-DSA-44 verify`	`38251` cycles	`38172` cycles	`1.00`
`ML-DSA-65 keypair`	`61517` cycles	`62847` cycles	`0.98`
`ML-DSA-65 sign`	`199619` cycles	`202327` cycles	`0.99`
`ML-DSA-65 verify`	`62330` cycles	`62804` cycles	`0.99`
`ML-DSA-87 keypair`	`94321` cycles	`94035` cycles	`1.00`
`ML-DSA-87 sign`	`231954` cycles	`231777` cycles	`1.00`
`ML-DSA-87 verify`	`94084` cycles	`94149` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i) (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`95220` cycles	`95219` cycles	`1.00`
`ML-DSA-44 sign`	`348692` cycles	`349266` cycles	`1.00`
`ML-DSA-44 verify`	`100860` cycles	`100928` cycles	`1.00`
`ML-DSA-65 keypair`	`164843` cycles	`165049` cycles	`1.00`
`ML-DSA-65 sign`	`567771` cycles	`568178` cycles	`1.00`
`ML-DSA-65 verify`	`165663` cycles	`165297` cycles	`1.00`
`ML-DSA-87 keypair`	`267616` cycles	`268215` cycles	`1.00`
`ML-DSA-87 sign`	`722497` cycles	`723212` cycles	`1.00`
`ML-DSA-87 verify`	`271964` cycles	`271850` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

SpacemiT K1 8 (Banana Pi F3) benchmarks (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`822407` cycles	`823326` cycles	`1.00`
`ML-DSA-44 sign`	`3324827` cycles	`3323407` cycles	`1.00`
`ML-DSA-44 verify`	`918875` cycles	`918360` cycles	`1.00`
`ML-DSA-65 keypair`	`1400141` cycles	`1397290` cycles	`1.00`
`ML-DSA-65 sign`	`5440333` cycles	`5447893` cycles	`1.00`
`ML-DSA-65 verify`	`1466189` cycles	`1465482` cycles	`1.00`
`ML-DSA-87 keypair`	`2300570` cycles	`2302142` cycles	`1.00`
`ML-DSA-87 sign`	`6837239` cycles	`6830077` cycles	`1.00`
`ML-DSA-87 verify`	`2408928` cycles	`2401423` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`69037` cycles	`69148` cycles	`1.00`
`ML-DSA-44 sign`	`185286` cycles	`185205` cycles	`1.00`
`ML-DSA-44 verify`	`69115` cycles	`69058` cycles	`1.00`
`ML-DSA-65 keypair`	`119379` cycles	`119551` cycles	`1.00`
`ML-DSA-65 sign`	`295678` cycles	`295903` cycles	`1.00`
`ML-DSA-65 verify`	`115352` cycles	`115424` cycles	`1.00`
`ML-DSA-87 keypair`	`202628` cycles	`201400` cycles	`1.01`
`ML-DSA-87 sign`	`386087` cycles	`386017` cycles	`1.00`
`ML-DSA-87 verify`	`194381` cycles	`193469` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`56954` cycles	`56664` cycles	`1.01`
`ML-DSA-44 sign`	`180571` cycles	`180626` cycles	`1.00`
`ML-DSA-44 verify`	`61319` cycles	`61207` cycles	`1.00`
`ML-DSA-65 keypair`	`100215` cycles	`99313` cycles	`1.01`
`ML-DSA-65 sign`	`297386` cycles	`296519` cycles	`1.00`
`ML-DSA-65 verify`	`100077` cycles	`100165` cycles	`1.00`
`ML-DSA-87 keypair`	`153515` cycles	`153618` cycles	`1.00`
`ML-DSA-87 sign`	`353753` cycles	`352593` cycles	`1.00`
`ML-DSA-87 verify`	`152841` cycles	`152439` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton3

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`73802` cycles	`73799` cycles	`1.00`
`ML-DSA-44 sign`	`228477` cycles	`228622` cycles	`1.00`
`ML-DSA-44 verify`	`78190` cycles	`78120` cycles	`1.00`
`ML-DSA-65 keypair`	`129705` cycles	`129706` cycles	`1.00`
`ML-DSA-65 sign`	`378376` cycles	`378331` cycles	`1.00`
`ML-DSA-65 verify`	`129087` cycles	`129146` cycles	`1.00`
`ML-DSA-87 keypair`	`208796` cycles	`210583` cycles	`0.99`
`ML-DSA-87 sign`	`475046` cycles	`479573` cycles	`0.99`
`ML-DSA-87 verify`	`208636` cycles	`210173` cycles	`0.99`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`115337` cycles	`115305` cycles	`1.00`
`ML-DSA-44 sign`	`377258` cycles	`377922` cycles	`1.00`
`ML-DSA-44 verify`	`120610` cycles	`120479` cycles	`1.00`
`ML-DSA-65 keypair`	`199264` cycles	`199318` cycles	`1.00`
`ML-DSA-65 sign`	`624410` cycles	`623033` cycles	`1.00`
`ML-DSA-65 verify`	`198444` cycles	`198396` cycles	`1.00`
`ML-DSA-87 keypair`	`326635` cycles	`326190` cycles	`1.00`
`ML-DSA-87 sign`	`791718` cycles	`790700` cycles	`1.00`
`ML-DSA-87 verify`	`325574` cycles	`324830` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`41811` cycles	`42681` cycles	`0.98`
`ML-DSA-44 sign`	`132382` cycles	`130516` cycles	`1.01`
`ML-DSA-44 verify`	`45305` cycles	`44449` cycles	`1.02`
`ML-DSA-65 keypair`	`73719` cycles	`72663` cycles	`1.01`
`ML-DSA-65 sign`	`213014` cycles	`212363` cycles	`1.00`
`ML-DSA-65 verify`	`73695` cycles	`73091` cycles	`1.01`
`ML-DSA-87 keypair`	`110060` cycles	`109973` cycles	`1.00`
`ML-DSA-87 sign`	`251189` cycles	`249309` cycles	`1.01`
`ML-DSA-87 verify`	`111007` cycles	`110662` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'AMD EPYC 4th gen (c7a)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9531203`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`44170` cycles	`42681` cycles	`1.03`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a) (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`135022` cycles	`134917` cycles	`1.00`
`ML-DSA-44 sign`	`539702` cycles	`539598` cycles	`1.00`
`ML-DSA-44 verify`	`148019` cycles	`147999` cycles	`1.00`
`ML-DSA-65 keypair`	`228235` cycles	`228399` cycles	`1.00`
`ML-DSA-65 sign`	`889365` cycles	`889693` cycles	`1.00`
`ML-DSA-65 verify`	`237713` cycles	`238055` cycles	`1.00`
`ML-DSA-87 keypair`	`373476` cycles	`373632` cycles	`1.00`
`ML-DSA-87 sign`	`1108160` cycles	`1108416` cycles	`1.00`
`ML-DSA-87 verify`	`387641` cycles	`388237` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i) (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`159276` cycles	`157991` cycles	`1.01`
`ML-DSA-44 sign`	`569781` cycles	`566743` cycles	`1.01`
`ML-DSA-44 verify`	`171379` cycles	`169525` cycles	`1.01`
`ML-DSA-65 keypair`	`271267` cycles	`271800` cycles	`1.00`
`ML-DSA-65 sign`	`928634` cycles	`930949` cycles	`1.00`
`ML-DSA-65 verify`	`276291` cycles	`277142` cycles	`1.00`
`ML-DSA-87 keypair`	`453061` cycles	`451994` cycles	`1.00`
`ML-DSA-87 sign`	`1185150` cycles	`1183143` cycles	`1.00`
`ML-DSA-87 verify`	`462360` cycles	`460949` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`115204` cycles	`114988` cycles	`1.00`
`ML-DSA-44 sign`	`377148` cycles	`377311` cycles	`1.00`
`ML-DSA-44 verify`	`120491` cycles	`120175` cycles	`1.00`
`ML-DSA-65 keypair`	`199022` cycles	`199169` cycles	`1.00`
`ML-DSA-65 sign`	`624045` cycles	`622748` cycles	`1.00`
`ML-DSA-65 verify`	`198186` cycles	`198196` cycles	`1.00`
`ML-DSA-87 keypair`	`326157` cycles	`325588` cycles	`1.00`
`ML-DSA-87 sign`	`791080` cycles	`789931` cycles	`1.00`
`ML-DSA-87 verify`	`325132` cycles	`324373` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton3 (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`138429` cycles	`138307` cycles	`1.00`
`ML-DSA-44 sign`	`493286` cycles	`493495` cycles	`1.00`
`ML-DSA-44 verify`	`148415` cycles	`148340` cycles	`1.00`
`ML-DSA-65 keypair`	`241696` cycles	`241530` cycles	`1.00`
`ML-DSA-65 sign`	`809838` cycles	`809805` cycles	`1.00`
`ML-DSA-65 verify`	`240591` cycles	`240580` cycles	`1.00`
`ML-DSA-87 keypair`	`396077` cycles	`395694` cycles	`1.00`
`ML-DSA-87 sign`	`1027664` cycles	`1027092` cycles	`1.00`
`ML-DSA-87 verify`	`401788` cycles	`401276` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a) (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`121283` cycles	`120184` cycles	`1.01`
`ML-DSA-44 sign`	`456240` cycles	`454855` cycles	`1.00`
`ML-DSA-44 verify`	`131066` cycles	`130119` cycles	`1.01`
`ML-DSA-65 keypair`	`205703` cycles	`205112` cycles	`1.00`
`ML-DSA-65 sign`	`737746` cycles	`736185` cycles	`1.00`
`ML-DSA-65 verify`	`210732` cycles	`210763` cycles	`1.00`
`ML-DSA-87 keypair`	`338822` cycles	`338436` cycles	`1.00`
`ML-DSA-87 sign`	`933840` cycles	`930453` cycles	`1.00`
`ML-DSA-87 verify`	`350327` cycles	`350134` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`69529` cycles	`69304` cycles	`1.00`
`ML-DSA-44 sign`	`215134` cycles	`215291` cycles	`1.00`
`ML-DSA-44 verify`	`72826` cycles	`72669` cycles	`1.00`
`ML-DSA-65 keypair`	`123077` cycles	`122773` cycles	`1.00`
`ML-DSA-65 sign`	`353781` cycles	`353606` cycles	`1.00`
`ML-DSA-65 verify`	`120777` cycles	`120708` cycles	`1.00`
`ML-DSA-87 keypair`	`201363` cycles	`200422` cycles	`1.00`
`ML-DSA-87 sign`	`451743` cycles	`451833` cycles	`1.00`
`ML-DSA-87 verify`	`198439` cycles	`198481` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2 (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`213473` cycles	`213791` cycles	`1.00`
`ML-DSA-44 sign`	`782953` cycles	`795734` cycles	`0.98`
`ML-DSA-44 verify`	`230078` cycles	`230270` cycles	`1.00`
`ML-DSA-65 keypair`	`384309` cycles	`385066` cycles	`1.00`
`ML-DSA-65 sign`	`1308829` cycles	`1308835` cycles	`1.00`
`ML-DSA-65 verify`	`375524` cycles	`376464` cycles	`1.00`
`ML-DSA-87 keypair`	`607752` cycles	`605935` cycles	`1.00`
`ML-DSA-87 sign`	`1629185` cycles	`1626204` cycles	`1.00`
`ML-DSA-87 verify`	`619721` cycles	`617553` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4 (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`132704` cycles	`132772` cycles	`1.00`
`ML-DSA-44 sign`	`498139` cycles	`498169` cycles	`1.00`
`ML-DSA-44 verify`	`144789` cycles	`144900` cycles	`1.00`
`ML-DSA-65 keypair`	`226615` cycles	`226216` cycles	`1.00`
`ML-DSA-65 sign`	`812892` cycles	`812288` cycles	`1.00`
`ML-DSA-65 verify`	`231649` cycles	`231591` cycles	`1.00`
`ML-DSA-87 keypair`	`374746` cycles	`374548` cycles	`1.00`
`ML-DSA-87 sign`	`1021485` cycles	`1020870` cycles	`1.00`
`ML-DSA-87 verify`	`383785` cycles	`383507` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`213088` cycles	`213101` cycles	`1.00`
`ML-DSA-44 sign`	`783050` cycles	`782017` cycles	`1.00`
`ML-DSA-44 verify`	`229821` cycles	`230313` cycles	`1.00`
`ML-DSA-65 keypair`	`383988` cycles	`384148` cycles	`1.00`
`ML-DSA-65 sign`	`1327414` cycles	`1315035` cycles	`1.01`
`ML-DSA-65 verify`	`375351` cycles	`375718` cycles	`1.00`
`ML-DSA-87 keypair`	`606680` cycles	`605250` cycles	`1.00`
`ML-DSA-87 sign`	`1623239` cycles	`1622964` cycles	`1.00`
`ML-DSA-87 verify`	`618648` cycles	`617448` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`287880` cycles	`281879` cycles	`1.02`
`ML-DSA-44 sign`	`938716` cycles	`923696` cycles	`1.02`
`ML-DSA-44 verify`	`292269` cycles	`289884` cycles	`1.01`
`ML-DSA-65 keypair`	`486374` cycles	`479627` cycles	`1.01`
`ML-DSA-65 sign`	`1518184` cycles	`1503826` cycles	`1.01`
`ML-DSA-65 verify`	`480606` cycles	`470998` cycles	`1.02`
`ML-DSA-87 keypair`	`843318` cycles	`821761` cycles	`1.03`
`ML-DSA-87 sign`	`2063488` cycles	`2022955` cycles	`1.02`
`ML-DSA-87 verify`	`827690` cycles	`807224` cycles	`1.03`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A55 (Snapdragon 888) benchmarks (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`465092` cycles	`460738` cycles	`1.01`
`ML-DSA-44 sign`	`2223370` cycles	`2206928` cycles	`1.01`
`ML-DSA-44 verify`	`546678` cycles	`544792` cycles	`1.00`
`ML-DSA-65 keypair`	`777623` cycles	`772159` cycles	`1.01`
`ML-DSA-65 sign`	`3627698` cycles	`3610816` cycles	`1.00`
`ML-DSA-65 verify`	`852507` cycles	`845380` cycles	`1.01`
`ML-DSA-87 keypair`	`1261291` cycles	`1249178` cycles	`1.01`
`ML-DSA-87 sign`	`4520350` cycles	`4476210` cycles	`1.01`
`ML-DSA-87 verify`	`1373327` cycles	`1359515` cycles	`1.01`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`239934` cycles	`234090` cycles	`1.02`
`ML-DSA-44 sign`	`711541` cycles	`692935` cycles	`1.03`
`ML-DSA-44 verify`	`245469` cycles	`238904` cycles	`1.03`
`ML-DSA-65 keypair`	`425922` cycles	`394503` cycles	`1.08`
`ML-DSA-65 sign`	`1183873` cycles	`1101766` cycles	`1.07`
`ML-DSA-65 verify`	`408843` cycles	`383121` cycles	`1.07`
`ML-DSA-87 keypair`	`685480` cycles	`654376` cycles	`1.05`
`ML-DSA-87 sign`	`1525553` cycles	`1443114` cycles	`1.06`
`ML-DSA-87 verify`	`679303` cycles	`639868` cycles	`1.06`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-65 keypair`	`425922` cycles	`394503` cycles	`1.08`
`ML-DSA-65 sign`	`1183873` cycles	`1101766` cycles	`1.07`
`ML-DSA-65 verify`	`408843` cycles	`383121` cycles	`1.07`
`ML-DSA-87 keypair`	`685480` cycles	`654376` cycles	`1.05`
`ML-DSA-87 sign`	`1525553` cycles	`1443114` cycles	`1.06`
`ML-DSA-87 verify`	`679303` cycles	`639868` cycles	`1.06`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Benchmark suite	Current: `9531203`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`313238` cycles	`315723` cycles	`0.99`
`ML-DSA-44 sign`	`1209928` cycles	`1218394` cycles	`0.99`
`ML-DSA-44 verify`	`332321` cycles	`342440` cycles	`0.97`
`ML-DSA-65 keypair`	`563275` cycles	`560329` cycles	`1.01`
`ML-DSA-65 sign`	`1933419` cycles	`1961671` cycles	`0.99`
`ML-DSA-65 verify`	`522699` cycles	`527254` cycles	`0.99`
`ML-DSA-87 keypair`	`877032` cycles	`863010` cycles	`1.02`
`ML-DSA-87 sign`	`2491550` cycles	`2430392` cycles	`1.03`
`ML-DSA-87 verify`	`885890` cycles	`880232` cycles	`1.01`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Benchmark suite	Current: `32d897d`	Previous: `f7fccd9`	Ratio
`ML-DSA-44 keypair`	`310892` cycles	`315723` cycles	`0.98`
`ML-DSA-44 sign`	`1180062` cycles	`1218394` cycles	`0.97`
`ML-DSA-44 verify`	`336194` cycles	`342440` cycles	`0.98`
`ML-DSA-65 keypair`	`559647` cycles	`560329` cycles	`1.00`
`ML-DSA-65 sign`	`1926617` cycles	`1961671` cycles	`0.98`
`ML-DSA-65 verify`	`535382` cycles	`527254` cycles	`1.02`
`ML-DSA-87 keypair`	`845971` cycles	`863010` cycles	`0.98`
`ML-DSA-87 sign`	`2418850` cycles	`2430392` cycles	`1.00`
`ML-DSA-87 verify`	`866119` cycles	`880232` cycles	`0.98`

This comment was automatically generated by workflow using github-action-benchmark.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

1. Weaken post-condition and loop invariant in polyvecl_add(). The stonger post-condition was unncessary. 2. Simplify polyvec_matrix_expand(). Small performance loss here since batched_seeds[] is (re-) initialized every time. This is bit slower but removes a loop statement entirely. 3. Refactor polyvec_pointwise_acc_montgomery() by splitting core "sum of products" calculation into a distinct local function mld_pointwise_sum_of_products(). Add proof of the latter. Proof time for parameter set 87 now 4 minutes (real-time) and 40 minutes (user time) with 64 cores on an r7g instance. Signed-off-by: Rod Chapman <[email protected]>

1. Weaken the contract of mld_polyveck_add(). This is sufficient to prove the caller in mld_attempt_signature_generation() 2. Introduce a new mld_polyveck_add_error() with stronger contracts where the second argument is an error term where all coefficients are bounded in absolute value to MLDSA_ETA. The post-condition of this function is just right to prove the calling code in crypto_sign_keypair_internal() which relies on these stronger bounds. 3. Add proof artefacts as appropriate. Signed-off-by: Rod Chapman <[email protected]>

Signed-off-by: Rod Chapman <[email protected]>

to simplify polyvec_maxtrix_expand(), stabilize proof and avoid need to ignore code for proof. Signed-off-by: Rod Chapman <[email protected]>

mkannwischer commented Nov 5, 2025

View reviewed changes

mldsa/src/polyvec.c Outdated Show resolved Hide resolved

mkannwischer mentioned this pull request Nov 5, 2025

Add MLD_CONFIG_SERIAL_FIPS202_ONLY option #558

Draft

mkannwischer marked this pull request as ready for review November 5, 2025 03:45

mkannwischer requested a review from a team as a code owner November 5, 2025 03:45

hanno-becker added the DO-NOT-MERGE label Nov 5, 2025

rod-chapman self-assigned this Nov 5, 2025

rod-chapman added the benchmark label Nov 5, 2025